Verification engineers and managers of chip design projects need tools for planning, controlling progress, and declaring sign-off of functional verification. Various coverage metrics for measuring progress and completion of functional verification of RTL design of components of systems on chips are well established for simulation-based verification.
In recent years, experience with formal property-checkers has shown that formal verification as an alternative approach is more efficient and exhaustive than simulation for a range of verification tasks. Therefore, mixed verification environments with simulation and formal verification tools are used more frequently in design projects.
However, the combination of mixed verification approaches is still unclear, as, finally, quantification and combination of all verification results is required, regardless of which verification technology has been applied to a verification task. In addition, formal property checking methodologies shall provide compatible metrics usable and interpretable by project managers without in-depth expertise in formal methods.
While completeness and coverage of formal properties have already been addressed, sufficient efficiency of formal property coverage measurement, which is crucial for any productive verification of industrial RTL designs, has not yet been gained. Thus, common formal property qualification approaches are based on very weak coverage notions, are limited to small applications, or still suffer from run-times hardly acceptable in productive chip design project schedules. This inefficiency of formal property qualification is still a major obstacle for wider acceptance and exploitation of the potentials of formal property-checking technology in industrial chip-design.
One general qualification approach for formal properties is based on injection of faults into designs and checking whether the injected faults are detected by the properties. If the detection of each fault is related to the coverage of a corresponding piece of code, the ratio of all faults detected by a set of properties to all injected faults is an appropriate measure of the overall code coverage by the set of properties, and in addition provides information of design parts not sufficiently addressed by verification.
While fault injection for the purpose of coverage analysis itself is conceptually well understood, the feasibility and efficiency of such qualification approaches in industrial chip design projects is a problem, because a potentially very large number of combinations of faults and test-cases/properties needs to be checked within the typically very tight schedule of chip development.
Therefore, there e.g. exists a need for an improved method and system for formal fault detection, in particular, for formal fault detection in an instrumented model of a register-transfer-level (RTL) design.